x<y
L.P(x;y)) == x, y:T. x before y L 
P(x;y)
clarification:
l_all2(L;T;x,y.P(x;y)) ==
x:T, y:T. x before y L T P(x;y) | 4,23 |
x<yL.P(x;y)) == x, y:T. x before y L P(x;y)
x:T, y:T. x before y L T P(x;y)
| Definitions | x:A. B(x) Q l |
| FDL editor aliases | l_all2 |